(*
This file is part of the Lustre reader

* Copyright (c) 2010, Nicola Camuffo.
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are met:
*     * Redistributions of source code must retain the above copyright
*       notice, this list of conditions and the following disclaimer.
*     * Redistributions in binary form must reproduce the above copyright
*       notice, this list of conditions and the following disclaimer in the
*       documentation and/or other materials provided with the distribution.
*     * Neither the name of Nicola Camuffo, nor the
*       names of its contributors may be used to endorse or promote products
*       derived from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDER ''AS IS'' AND ANY
* EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER BE LIABLE FOR ANY
* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
* (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
* LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)


open Lustypes
open Lustables
open Exceptions
open Comparation



(* verifies if the expression is boolean. *)
let verify_boolean (_,t) =
  let msg = "Expression has not boolean type." in
	match t with
		T_BOOL -> ()
		| T_TOCHECK -> ()
		| _ -> raise (Type_mismatch_exception (msg,None))


(* verifies if the expression is integer. *)
let verify_integer (_,t) =
  let msg = "Expression has not integer type." in
	match t with
		T_INT -> ()
		| T_TOCHECK -> ()
		| _ -> raise (Type_mismatch_exception (msg,None))

  
(* verifies if the expression is integer or real. *)
let verify_numeric (_,t) =
  let msg = "Expression has not numeric type." in
	match t with
		T_INT | T_REAL -> ()
		| T_TOCHECK -> ()
		| _ -> raise (Type_mismatch_exception (msg,None))


(* verifies if the espression is a tuple. *)
let verify_tuple (_,t) =
  let msg = "Expression has not tuple type." in
	match t with
		T_TUPLE(_) -> ()
		| T_TOCHECK -> ()
		| _ -> raise (Type_mismatch_exception (msg,None))


(* verifies if the espression is a struct. *)
let verify_struct (_,t) =
  let msg = "Expression has not struct type." in
	match t with
		T_STRUCT(_) -> ()
		| T_TOCHECK -> ()
		| _ -> raise (Type_mismatch_exception (msg,None))



(* catches-and-throws *)
let cat f msg =
	try
		f ()
	with exn -> raise (Type_mismatch_exception (msg,Some exn))
	
			
(* verifies if both expressions are boolean. returns boolean type *)
let match_types_boolean (_,t1) (_,t2) =
	let msg1 = "Expressions are incompatible." in
  let msg2 = "At least one expression has not boolean type." in
	
	let tp = cat (fun _ -> deep_match_types t1 t2) msg1 in
	match tp with
		T_BOOL -> tp
		| T_TOCHECK -> tp
		| _ -> raise (Type_mismatch_exception (msg2,None))


(* verifies if both expressions are integer. returns integer type *)
let match_types_integer (_,t1) (_,t2) =
	let msg1 = "Expressions are incompatible." in
  let msg2 = "At least one expression has not integer type." in
	
	let tp = cat (fun _ -> deep_match_types t1 t2) msg1 in
	match tp with
		T_INT -> tp
		| T_TOCHECK -> tp
		| _ -> raise (Type_mismatch_exception (msg2,None))


(* verifies if both expressions are integer or real. returns integer or real type *)
let match_types_numeric (_,t1) (_,t2) =
	let msg1 = "Expressions are incompatible." in
  let msg2 = "At least one expression has not numeric type." in
	
	let tp = cat (fun _ -> deep_match_types t1 t2) msg1 in
	match tp with
		T_INT | T_REAL -> tp
		| T_TOCHECK -> tp
		| _ -> raise (Type_mismatch_exception (msg2,None))


(* verifies if both expressions are comparable using '<', '>', '<=', '>='. returns boolean type *)
let match_types_ltge (_,t1) (_,t2) =
	let msg1 = "Expressions are incompatible." in
  let msg2 = "At least one expression has not numeric type." in
	
	let tp = cat (fun _ -> deep_match_types t1 t2) msg1 in
	match tp with
		T_INT | T_REAL -> T_BOOL
		| T_TOCHECK -> T_TOCHECK
		| _ -> raise (Type_mismatch_exception (msg2,None))


(* verifies if both expressions are comparable using '=', '<>'. returns boolean type *)
let match_types_equals (_,t1) (_,t2) =
	let msg1 = "Expressions are incompatible." in
  let msg2 = "At least one expression has not numeric type." in
	
	let tp = cat (fun _ -> deep_match_types t1 t2) msg1 in
	match tp with
		T_INT | T_REAL | T_BOOL -> T_BOOL
		| T_TOCHECK -> tp
		| _ -> raise (Type_mismatch_exception (msg2,None))


(* verifies if the three expressions are compatible for a 'if-then-else' form: then first one must be boolean and the other of same type.
   returns type of the two branchs *)
let match_types_ite e1 (_,t2) (_,t3) =
  let msg1 = "Condition expression has not boolean type." in
  let msg2 = "Branches expressions have not same type." in

	cat (fun _ -> verify_boolean e1) msg1;
	cat (fun _ -> deep_match_types t2 t3) msg2


(* verifies if the expressions are compatible for a 'e1 -> e2' form. returns type of the expressions (same type) *)
let match_types_follby (_,t1) (_,t2) =
  let msg = "Expressions have not same type." in
	cat (fun _ -> deep_match_types t1 t2) msg


(* verifies if the expressions are compatible for a 'e when c' form. returns type of the first expression *)
let match_types_clocked e1 e2 =
  let msg = "Clock expression has not boolean type." in
  let t = snd e1 in

	cat (fun _ -> verify_boolean e2) msg;
	t

(* verifies if the expressions are compatible for a '#(e1,e2,..en)' or 'nor(e1,e2,..en)' form. returns boolean type *)
let match_types_bool_nary el =
  let msg = "Not all expressions have boolean type." in

	cat (fun _ -> 
    List.iter (fun e -> verify_boolean e) el;
		if (List.exists (fun (_,t) -> t = T_TOCHECK) el) then T_TOCHECK else T_BOOL
	) msg

(* given an expression list and a type list, verifies if expressions are compatible with types *)
let match_types_node_params el tl =
  let msg1 = "Expression types incompatible with node parameters types." in
	let msg2 = "Different number of expressions and node parameters." in
	
  try
    List.iter2 (fun (_,et) t ->
      ignore (deep_match_types et t)
    ) el tl
  with
		Type_mismatch_exception (_,_) as exn -> raise (Type_mismatch_exception (msg1,Some exn))
		| Invalid_argument _ as exn -> raise (Type_mismatch_exception (msg2,Some exn))


(* verifies if the lhs and the expression are compatible. *)
let match_types_for_assignment (_,lhst) (_,rhst) =
  let msg = "Lhs and rhs are not compatible." in
	ignore (cat (fun _ -> deep_match_types lhst rhst) msg)
		
